Conformal Geometric Algebra (CGA), as an advanced geometric representation and computing system, provides a concise, intuitive, and unified homogeneous algebraic framework for classical geometry. CGA represents the reference origin (e0) and a point at infinity (e∞) by adding two dimensions, so that the Euclidean space is embedded into a conformal space, and gives it the structure of a Minkowski inner product, not only preserving the Grassmann structure of an outer product in homogeneous space, but also making the inner product possess a definite geometric meaning characterizing the basic metric of the distance, angle, and so on. CGA not only succeeds in solving the problem of how to accomplish geometric computations with geometric language, but also plays a key role in solving geometric problems in many high-technology fields, such as engineering and computer science. In robotics, CGA is different from the previously used algebra in that an object involved in its computation is a geometry instead of a number. The object in robot research is a geometric relation formed by a system established based on a basic geometry. Therefore, conformal geometric algebra is unique in robot research.
At present, modeling, computation and analysis are performed using CGA as a mathematical tool. In this process, computer-based numerical computation and analysis and computer algebra systems (CASs) (e.g., Maple, CLUCaic, Gaalop, etc.) are usually used. However, neither of these two methods can completely ensure the correctness and accuracy of the results. Because the number of iterations needed in the computation is limited by the computer memory and floating point numbers, numerical computation and analysis cannot completely ensure the accuracy of the results. However, although the symbolic method provided by CASs can accurately deduce the solution to a symbolic expression using a core algorithm, the algorithm for computing an enormous set of symbols has yet to be verified and there is a shortcoming in the processing of boundary conditions. Thus, the results that are obtained may still be problematic.
In recent decades, formal methods are widely used in many fields. With the development of basic research and the promotion of technological progress, new methods and new tools are continuously emerging, and have gradually improved into mature and highly reliable verification technologies. The main idea behind such technologies is to prove, based on mathematical theory, that the system that has been designed meets the system specifications or has the desired properties. Compared with a pen and paper-based manual analysis and the above traditional methods, formal methods can increase the chances of finding small but crucial errors in early designs, according to the stringency of mathematical logic.
The problems mentioned earlier arise when modeling, computation, and analysis are performed using CGA as a mathematical tool. A formal analysis of CGA theory is an ideal way to prevent such problems. Because CGA is unique in robot research, how to combine CGA with a formal way is an urgent technical problem that needs to be solved in robot research.